(** 
    The static interpreter for the Gnarly Programming Language. The contents of this file are designed to typecheck the abstract syntax tree of
    a Gnarly program, so many of the constructs of {i gnexp} have their own typechecking functions.
    @author mmvitousek
*)

open Gnsyn
open Printing
open List
exception ListLengthMismatch
exception StaticTypeException of gntype

(** 
    Main entry point for static interpreter. Either typechecks the provided program, sends an ancilliary file to the provided evaluator to typecheck (and 
    record type signatures in the environment), or a Nil type to represent the end of a program or an empty program. 
    @param program a {i gnarly} expression to be typechecked
    @param environment the current type environment
    @param type_file a function to typecheck additional files, e.g. libraries
    @return a value of {i gntype}
*)
let rec static_interpret program environment = 
	match program with
		  Empty			-> Basic_Type("Nil")
		| Expression(exp)	-> static_eval environment exp
		| Library(stng)		-> Basic_Type("Nil")
		| Syntax_Error          -> Basic_Type("Nil")
and static_eval env exp = 
	match exp with
		  Real(number)			-> Basic_Type("Real")
		| Integer(number)		-> Basic_Type("Int")
		| Boolean(boole)	        -> Basic_Type("Boolean")
		| Char(chr)			-> Basic_Type("Char")
		| Nil				-> List_Type(Empty_List)
		| Identifier(strng)		-> lookup env strng
		| Lambda(vars, ltype, expr)	-> eval_closure env vars ltype expr exp
		| Application(funexpr, args)	-> eval_application env funexpr args exp
		| Let(terms, rest)      	-> eval_let env terms rest exp
		| Commit(terms)		        -> eval_commit env terms exp
		| Sequence(expr1,expr2)		-> eval_seq env expr1 expr2 exp
		| Conditional(cond, truthbranch, falsebranch,check)
			-> eval_cond env cond truthbranch falsebranch check exp
		| Match(target, cases, default,check)	
			-> eval_match env target cases default check exp
and match_types type1 type2 = (* note: this relation is commutative but NOT TRANSITIVE *)
	let rec match_noncommute t1 t2 =
		match t1, t2 with
			  Static_Type_Error(_), _               -> false
			| Dynamic_Type, Static_Type_Error(_)    -> false
			| Dynamic_Type, _			-> true
			| List_Type(Empty_List), List_Type(_)	-> true
			| _, _					-> false
	and match_commutative t1 t2 =
		match t1, t2 with
			  Basic_Type(b1), Basic_Type(b2)		-> b1 = b2
			| List_Type(List(l1)), List_Type(List(l2))	-> match_types l1 l2
			| Product_Type(p1), Product_Type(p2)		-> match_prod p1 p2
			| Arrow_Type(v1, r1), Arrow_Type(v2, r2)	-> (match_types r1 r2) && (match_prod v1 v2)
			| _, _						-> false
	in (match_noncommute type1 type2) || (match_noncommute type2 type1) || (match_commutative type1 type2)
and match_prod p1 p2 =
	match p1, p2 with
		  t1::t1s, t2::t2s	-> (match_types t1 t2) && (match_prod t1s t2s)
		| [], []		-> true
		| _, _			-> false
and choose_return e1 e2 = 
	match e1, e2 with
		  Static_Type_Error(_), _			-> e1
		| _, Static_Type_Error(_)			-> e2
		| Dynamic_Type, _				-> e2
		| _, Dynamic_Type				-> e1
		| List_Type(Empty_List), List_Type(List(_))	-> e2
		| List_Type(List(_)), List_Type(Empty_List)	-> e1
		| _, _						-> e1
and extend_tenv env k v = 
	match (!env) with
		  TEnv(en) -> ref (TEnv((k, (ref v))::(en)))
and excise_tenv env k =
	match (!env) with
		  TEnv(en) -> ref (TEnv(remove_assoc k en))
and multi_extend_tenv env ks vs = 
	match ks, vs with
		  kk::kks, vv::vvs	-> multi_extend_tenv (extend_tenv env kk vv) kks vvs
		| [], []		-> env
		| _, _			-> raise ListLengthMismatch
and lookup env x = 
	match (!env) with TEnv(en) -> (try !(assoc x en) with Not_found -> Static_Type_Error("Undefined identifier " ^ x))
and choose_error vl err = 
	match vl with 
		  Static_Type_Error(_) -> vl
		| _                    -> err
and eval_closure env vars typ expr cexp = 
	let fake_dyns lst = 
		let rec dynloop i = 
			if i > 0 then Dynamic_Type::(dynloop (i - 1)) else []
		in dynloop (length lst)
	in match typ with 
		  Arrow_Type(vt, rt)	-> 
			  let eexpr = (static_eval (multi_extend_tenv env vars vt) expr)
			  in if match_types eexpr rt then typ 
				  else choose_error eexpr 
					(Static_Type_Error("Closure body has type " ^ (string_of_gntype eexpr) 
									  ^ " , expected type " ^ (string_of_gntype rt) 
									  ^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp)))
		| Dynamic_Type		-> 
			  let eexpr = (static_eval (multi_extend_tenv env vars (fake_dyns vars)) expr)
			  in (match eexpr with 
					Static_Type_Error(_)   -> eexpr
				      | _                      -> typ
			     )  
		| _			-> Static_Type_Error("Closure has type " ^ (string_of_gntype typ) ^ ", expects Dynamic or X -> X types" 
							     ^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))
and eval_application env fn args cexp =
	let rec eval_args env e =
		let ee = static_eval env e
		in match ee with
			  Static_Type_Error(_)	-> raise (StaticTypeException ee)
			| _			-> ee
	and eval_vars mapping argt argv =
		match argt, argv with 
			  tau::taus, exp::exps	-> eval_vars (append (eval_var tau exp) mapping) taus exps
			| [], []		-> mapping
			| _, []			-> raise (StaticTypeException (Static_Type_Error("Too few arguments provided to function application" 
												 ^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))))
			| [], _			-> raise (StaticTypeException (Static_Type_Error("Too many arguments provided to function application" 
												 ^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))))
	and fake_dyns lst = 
		let rec dynloop i = 
			if i > 0 then Dynamic_Type::(dynloop (i - 1)) else []
		in dynloop (length lst)
	and etv_member_match exp allow = fold_left (||) false (map (match_types exp) allow)
	and eval_var tau exp = 
		match tau, exp with
			  Type_Variable(s), _				-> (s,exp)::[]
			| Exclusive_Type_Variable(s, e), _		-> if etv_member_match exp e then (s, exp)::[] else []
			| Arrow_Type(vt, rt), Arrow_Type(ve, re)	-> append (eval_vars [] vt ve) (eval_var rt re)
			| Arrow_Type(vt, rt), Dynamic_Type		-> append (eval_vars [] vt (fake_dyns vt)) (eval_var rt Dynamic_Type)
			| Product_Type(pt), Product_Type(pe)		-> eval_vars [] pt pe
			| Product_Type(pt), Dynamic_Type		-> eval_vars [] pt (fake_dyns pt)
			| List_Type(List(lt)), List_Type(List(le))	-> eval_var lt le
			| List_Type(List(lt)), Dynamic_Type		-> eval_var lt Dynamic_Type
			| _						-> []
	and type_solve mapping fixed = 
		match mapping with 
			  (s, tau)::maps -> (try ( 
						     let hist = assoc s fixed
						     in let ns = choose_return tau hist
						     in type_solve maps ((s, ns)::fixed)
					     ) with Not_found -> type_solve maps ((s, tau)::fixed))
			| []             -> fixed
	and lookup_typevals vall ts = try (assoc ts vall) 
						with Not_found -> raise (StaticTypeException (Static_Type_Error("Unmatched type variable " 
														^ ts ^ "\n\t\tIn expression: " 
														^ (string_of_gnexp cexp))))
	and fixvar var vals =
		match var with
			  Type_Variable(s)			-> lookup_typevals vals s
			| Exclusive_Type_Variable(s,allow)	-> lookup_typevals vals s
			| Product_Type(vars)			-> Product_Type(fixvars vars vals)
			| Arrow_Type(vars, rtype)		-> Arrow_Type(fixvars vars vals, fixvar rtype vals)
			| List_Type(List(vtype))		-> List_Type(List(fixvar vtype vals))
			| _					-> var
	and fixvars vars vals = map (fun x -> fixvar x vals) vars
	and efn = static_eval env fn
	in match efn with 
		  Arrow_Type(vt, rt)	-> ( try (
						     let eargs = map (eval_args env) args
						     in let tvars = type_solve (eval_vars [] vt eargs) []
						     in (*print_string ("\nK" ^ (fold_string_infix ", " "" 
										      (map (fun (s,exp) -> ("(" ^ s ^ " " ^ (string_of_gntype exp) ^ ")")) tvars)));
							*) 
						     let fixvt = fixvars vt tvars
						     in let fixrt = fixvar rt tvars
						     in if match_prod fixvt eargs then fixrt
							     else Static_Type_Error("Function application expects arguments of types " 
										    ^ (string_of_typelist fixvt) ^ ", given " ^ (string_of_typelist eargs) 
										    ^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp))
					     ) with StaticTypeException(x)	-> x
					   )
		| Static_Type_Error(_)	-> efn
		| Dynamic_Type		-> efn
		| _			-> Static_Type_Error("Applied term has type " ^ (string_of_gntype efn) 
							     ^ ", expected Dynamic or X -> X type \n\t\tIn expression: " ^ (string_of_gnexp cexp))
and eval_let env terms rest cexp = 
	let eval_term tenv ((id, tau), value) = 
		let eval = static_eval tenv value
		in if match_types eval tau then ()
			else raise (StaticTypeException 
					    (choose_error eval (Static_Type_Error("Term assigned to " ^ id ^ " has type " 
										 ^ (string_of_gntype eval) ^ ", expected " ^ (string_of_gntype tau) 
										 ^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp))))
				   ); ()
	and ids, sigs = split (map fst terms)
	in let genv = multi_extend_tenv env ids sigs
	in try (
			iter (eval_term genv) terms;
			static_eval genv rest
		) with StaticTypeException(e) -> e
and eval_commit env terms cexp = 
	let eval_term tenv ((id, tau), value) = 
		let eval = static_eval tenv value
		in if match_types eval tau then ()
			else raise (StaticTypeException 
					    (choose_error eval (Static_Type_Error("Term assigned to " ^ id ^ " has type " 
										 ^ (string_of_gntype eval) ^ ", expected " ^ (string_of_gntype tau) 
										 ^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp))))
				   ); ()
	and ids, sigs = split (map fst terms)
	in let genv = multi_extend_tenv env ids sigs
	in try (
			iter (eval_term genv) terms;
			env := !genv;
			List_Type(Empty_List)
		) with StaticTypeException(e) -> e
and eval_seq env exp1 exp2 cexp = 
	let eexp1 = static_eval env exp1
	in match eexp1 with 
		  Static_Type_Error(_)	-> eexp1
		| _			-> static_eval env exp2
and eval_cond env cond tru fals check cexp = 
	let econd = static_eval env cond
	and etrue = static_eval env tru
	and efalse = static_eval env fals
	in match econd, etrue, efalse, check with
		  Static_Type_Error(_), _, _, _	        -> econd
		| _, Static_Type_Error(_), _, _	        -> etrue
		| _, _, Static_Type_Error(_), _	        -> efalse
		| _, _, _, false                        -> Dynamic_Type
		| Basic_Type("Boolean"), _, _, _	-> if match_types etrue efalse then choose_return etrue efalse 
		  else Static_Type_Error("Truth and false branches of conditional have types " ^ (string_of_gntype etrue)
					 ^ ", " ^ (string_of_gntype efalse) ^ ", which do not unify\n\t\tIn expression: "
					 ^ (string_of_gnexp cexp))
		| Dynamic_Type, _, _, _		        -> if match_types etrue efalse then choose_return etrue efalse 
		  else Static_Type_Error("Truth and false branches of conditional have types " ^ (string_of_gntype etrue) 
					 ^ ", " ^ (string_of_gntype efalse) ^ ", which do not unify\n\t\tIn expression: " 
					 ^ (string_of_gnexp cexp))
		| _, _, _, _			         -> Static_Type_Error("Branching term of conditional has type " ^ (string_of_gntype econd) 
								     ^ ", expected Boolean\n\t\tIn expression: " ^ (string_of_gnexp cexp))
and eval_match env target cases default check cexp = 
	let rec check_cases env cases mtype = map (fun (terms, exp) -> check_case env terms exp mtype) cases
	and extend_terms env terms mtype  = 
		match terms with 
			  x::[]	-> if x = "NIL" then env else extend_tenv env x (List_Type(List(mtype)))
			| x::xs	-> extend_terms (extend_tenv env x mtype) xs mtype
			| []	-> env
	and check_case env terms exp mtype =
		let eenv = extend_terms env terms mtype
		in let eeval = static_eval eenv exp
		in match eeval with
			  Static_Type_Error(_)	-> raise (StaticTypeException eeval)
			| _			-> eeval
	and match_all casetypes deftype =
		let match_each t ts = fold_left (&&) true (map (match_types t) ts)
		in match casetypes, check with
			  _, false      -> Dynamic_Type
			|  x::[], _	-> if match_types x deftype then choose_return x deftype
			  else Static_Type_Error("Inconsistent types for match cases: {" ^ (string_of_gntype x) ^ " * " ^ (string_of_gntype deftype) 
						 ^ "}\n\t\tIn expression: " ^ (string_of_gnexp cexp))
			| x::xs, _	        -> if (match_types x deftype) && (match_each x xs) then choose_return x (match_all xs deftype) 
			  else Static_Type_Error("Inconsistent types for match cases {" ^ (string_of_gntype x) ^ " * " ^ (string_of_typelist xs) 
						 ^ "  * " ^ (string_of_gntype deftype) ^ "}\n\t\tIn expression: " ^ (string_of_gnexp cexp))
			| _, _	        -> deftype
	in let etarg = static_eval env target
	and edef = static_eval env default
	in try (match etarg, edef with
			  Static_Type_Error(_), _	-> etarg
			| _, Static_Type_Error(_)	-> edef
			| List_Type(List(typ)), _	-> match_all (check_cases env cases typ) edef
			| Dynamic_Type, _		-> match_all (check_cases env cases Dynamic_Type) edef
			| List_Type(Empty_List), _	-> Static_Type_Error("Cannot match on empty list\n\t\tIn expression: " ^ (string_of_gnexp cexp))
			| _, _				-> Static_Type_Error("Attempting to match upon " ^ (string_of_gntype etarg) 
									     ^ ", expected target of List Type\n\t\tIn expression: " ^ (string_of_gnexp cexp))
	       ) with StaticTypeException(err)	-> err
